Static analysis based on abstract interpretation [See, e.g., P. Cousot and R. Cousot, “Static Determination of Dynamic Properties of Programs,” in International Symposium on Programming, pp. 106-126, 1976] and model checking [See, e.g., E. M. Clarke and E. A. Emerson, “Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic,” in Proceedings of Workshop on Logics of Programs, pp. 57-71, Springer, 1981; J. P. Quielle and J. Sifakis, “Specifications and Verification of Concurrent Systems in CESAR”, In Symposium on Programming, 1981] are popular techniques for program verification. They both rely on fixpoint computation, with the former heavily employing widening to ensure termination. [See, e.g., P. Cousot and N. Halbawachs, “Automatic Discovery of Linear Restraints Among Variables of a Program”, In Symposium on Principles of Programming Languages, pp. 84-96, 1978.]
The precision of a widening operator is crucial for the effectiveness of abstract interpretation. Often a widening operator is carefully designed by a user a priori for an abstract domain, and if it does not provide enough precision, the user either accepts the result as inconclusive or has to redesign the operator.
Widening for convex polyhedra was introduced for numerical relational analysis and later extended to verification of integer-valued programs and linear hybrid systems [See, e.g., N. Halbwachs, Y. E., Proy and P. Roumanoff, “Verification of Real-Time Systems Using Linear Relation Analysis”, Formal Methods in Systems Design, 11(2); 157-185, 1997]. The operator was generalized and subsequently applied to powersets (or finite unions) of convex polyhedra. [See, e.g., N. Halbwachs, “Delay Analysis in Synchronous Programs,” In Computer Aided Verification, pp. 333-346, Springer, 1993, LNCS 697; T. R. Gerber and W. Pugh, “Symbolic Model Checking of Infinite State Systems using Pressberger Arighmetic,” In Computer Aided Verification, pp. 400-411, Springer, 1997, LNCS 1254; R. Bagnara, P. M. Hill, and E. Zaffanella, “Widening Operators for Powerset Domains,” In Verification, Model Checking and Abstract Interpretation, pp. 135-148, Springer, 2004, LNCS 2937; and T. Bultan, R. Gerber, and C. League, “Verifying Systems with Integer Constraints and Boolean Predicates: A Composite Approach,” In International Symposium on Software Testing and Analysis, pp. 113-123, 1998] Approximation techniques were also studied where an extrapolation operator is introduced [See, e.g., T. A. Henzinger and P. H. Ho, “A Note on Abstract Interpretation Strategies for Hybrid Automata, “In Hybrid Systems II, pp 252-264, Springer 1995, LNCS 999. The difference between widening and extrapolation is that the latter does not guarantee termination. The widening precision can be increased by partitioning methods. [See, e.g, F. Bourdoncle, “Abstract Interpretation by Dynamic Partitioning”, J. Funct. Program., 2(4): 407-423, 1992; B. Jeannet, N. Halbwachs and P. Raymond, “Dynamic Partitioning in Analysis of Numerical Properties” In International Symposium on Static Analysis, pp. 39-50, Springer 2005,]. More recently, a widening operator was produced by combining several known heuristics and using convex widening as a last resort. [See, e.g., R. Bagnara, P. M. Hill, E. Ricci and E. Zaffanella, “Precise Widening Operators for Convex Polyhedra,” In International Symposium on Static Analysis”, pp. 337-354, Springer, 2004] In all of these previous works, no automatic refinement was involved.
In model checking, counterexample guided refinement [See., e.g., E. Clarke, O. Grumberg, S. Jha, Y. Lu and H. Veith, “Counterexample-guided Abstraction Refinement,” In Computer Aided Verification, pp. 154-169, Springer, 2000, LNCS 1855] has been used together with predicate abstraction [See, e.g., S. Graf and H. Saidi, “Construction of Abstract State Graphs with PVS,” In Computer Aided Verification, pp. 72-83, Springer 1997, LNCS 1254] to verify software programs [See, e.g., T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, “Lazy Abstraction”, In Principles of Programming Languages”, pp. 58-70, 2002; F. Ivanicic, I. Shlyakhter, A. Gupta, M. K. Ganai, Z. Yang, and P. Ashar”, “F-SOFT Software Verification Platform”, In Computer Aided Verification pp. 301-306, Springer, 2005, LNCS 3576].
As is known by those skilled in the art, predicate abstraction relies on finite sets of predicates to define abstract domains, and therefore can be viewed as an instance of domain refinement in abstract interpretation [R. Giacobazzi, F. Ranzato, and F. Scozzari, “Making Abstract Interpretations Complete”, J. ACM, 47(2):361-416, 2000]. However, finite abstractions in general are not as powerful as an infinite abstract domains with widening for Turing equivalent programming languages.
Recently [See, e.g., B. S. Gulavani and S. K. Rajamani, “Counterexample Driven Refinement for Abstract Interpretation”, In Tools and Algorithms for the Construction and Analysis of Systems, pp. 474-488, Springer, 2006, LNCS 3920], a counterexample driven refinement method for abstract interpretation has been proposed, which identifies the fixpoint steps at which precision loss happens due to widening in forward fixpoint computation, and then to use the least upper bound (convex hull for convex polyhedra) instead of widening at those steps. In effect, this refinement procedure simply skips the widening at particular steps (the least upper bound of two consecutive sets P and Q of a fixpoint computation is actually Q, since P⊂Q).